Description

Making progress towards symbolic jumpdestinations via SMT solving. This PR allows us to branch out to all potential jumpdests.

The system can restrict the returned value's number of relevant bytes to a fixed value. So if we are looking for a JUMP, it ignores high bytes, because it's impossible to have a PC that's more than 2^16 (more than 65K instructions). Similarly for addresses. This matters, because it can happen that there's some junk that's not restricted and we could get thousands of solutions, but they are actually all the same address if we ignore the bits other than the 160b that an address has.

Currently, it launches a new query for each new solution, which is very slow. This needs to be improved in a new PR. That will require a slight re-engineering of Solvers.hs, so we can query the system for more than one solution at a time.

Number of potential concrete is set to 10 by default. This is actually kinda low. However, we need to be a bit cautious, as things can blow up quickly, so I set 10. It can be changed via --max-branch K.

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog